COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	(get-proofs sl1)
C00011 00003	(DECL (U U0 U1 U2 U3 V V0 V1 V2 V3 W W0 W1 W2 W3) |GROUND| VARIABLE LIsTP)
C00014 ENDMK
C⊗;
(get-proofs sl1)
(proof samelength)

2. ∀U V.sL(U,V)≡NULL(U)∧NULL(V)∨¬NULL(U)∧¬NULL(V)∧sL(CDR(U),CDR(V))

3. (∀U X.sL(U,NNIL)⊃sL(CONs(X,U),NNIL*LIsT(X)))∧
   (∀X U.(∀U5 X.sL(U5,U)⊃sL(CONs(X,U5),U*LIsT(X)))⊃
          (λV.∀U X.sL(U,V)⊃sL(CONs(X,U),V*LIsT(X)))(CONs(X,U)))⊃
    (∀U U4 X.sL(U4,U)⊃sL(CONs(X,U4),U*LIsT(X)))

6. NULL(NNIL)

7. sL(U,NNIL)≡U=NNIL

8. sL(NNIL,NNIL)∧(∀X U.sL(U,U)⊃sL(CONs(X,U),CONs(X,U)))⊃(∀U.sL(U,U))

* 9. ∀U.sL(U,U)

10. ∀U.sL(U,NNIL)≡U=NNIL
    ctxt: (1 LIsPAX#1 LIsPAX#5)   deps: NIL
(deletel 3)

* 12. (∀U X.sL(U,NNIL)⊃sL(CONs(X,U),NNIL*LIsT(X)))∧
    (∀X U.(∀U3 X.sL(U3,U)⊃sL(CONs(X,U3),U*LIsT(X)))⊃
           (∀U2 X1.sL(U2,CONs(X,U))⊃sL(CONs(X1,U2),CONs(X,U)*LIsT(X1))))⊃
     (∀U U1 X.sL(U1,U)⊃sL(CONs(X,U1),U*LIsT(X)))
    ctxt: (1 12 LIsPAX#1 LIsPAX#2 LIsPAX#5 LIsPAX#6 LIsPAX#18 LIsPAX#22)
    deps: NIL

(decsimp |∀x u.sl(u,nnil) ⊃ cons(x,u) = nnil*list(x)| nil
(7 6 lispax#20 lispax#24) nil (lispax#12 lispax#23 lispax#19))

* 11. ∀X U.sL(U,NNIL)⊃CONs(X,U)=NNIL*LIsT(X)
    ctxt: (1 LIsPAX#1 LIsPAX#2 LIsPAX#5 LIsPAX#6 LIsPAX#18 LIsPAX#22)
    deps: NIL

(show)
(DECL (sL) |GROUND⊗GROUND→TRUTHVAL| CONsTANT)

(AXIOM |∀U V.sL(U,V)≡NULL(U)∧NULL(V)∨(¬NULL(U)∧¬NULL(V))∧sL(CDR(U),CDR(V))|)
2. ∀U V.sL(U,V)≡NULL(U)∧NULL(V)∨¬NULL(U)∧¬NULL(V)∧sL(CDR(U),CDR(V))
   ctxt: (1 LIsPAX#1 LIsPAX#7 LIsPAX#8)   deps: NIL

(∀E U |U| 2 |NIL|)
3. ∀V.sL(U,V)≡NULL(U)∧NULL(V)∨¬NULL(U)∧¬NULL(V)∧sL(CDR(U),CDR(V))
   ctxt: (1 LIsPAX#1 LIsPAX#7 LIsPAX#8)   deps: NIL

(∀E V |NNIL| 3 |NIL|)
4. sL(U,NNIL)≡NULL(U)∧NULL(NNIL)∨¬NULL(U)∧¬NULL(NNIL)∧sL(CDR(U),CDR(NNIL))
   ctxt: (1 LIsPAX#1 LIsPAX#5 LIsPAX#7 LIsPAX#8)   deps: NIL

(DECs |NULL(NNIL)| |$(U NNIL)#13*NIL|)
5. NULL(NNIL)
   ctxt: (LIsPAX#5 LIsPAX#8)   deps: NIL

(DECs |sL(U,NNIL)≡U=NNIL| |$(U NNIL)#13*NIL| 4 5)
6. sL(U,NNIL)≡U=NNIL
   ctxt: (1 LIsPAX#1 LIsPAX#5)   deps: NIL

(∀E PHI |λU.sL(U,U)| LIsPAX#17 |NIL| LIsPAX#12)
7. sL(NNIL,NNIL)∧(∀X U.sL(U,U)⊃sL(CONs(X,U),CONs(X,U)))⊃(∀U.sL(U,U))
   ctxt: (1 LIsPAX#1 LIsPAX#2 LIsPAX#5 LIsPAX#6)   deps: NIL

(DECs |∀U.sL(U,U)| |NIL| (7 2 6 5) NIL LIsPAX#12)
8. ∀U.sL(U,U)
   ctxt: (1 LIsPAX#1)   deps: NIL

(∀I (U) 6)
9. ∀U.sL(U,NNIL)≡U=NNIL
   ctxt: (1 LIsPAX#1 LIsPAX#5)   deps: NIL

(∀E PHI |λV.∀U X Y.sL(U,V)⊃sL(CONs(X,U),V*LIsT(X))| LIsPAX#17 |NIL| LIsPAX#12)
10. (∀U X.sL(U,NNIL)⊃sL(CONs(X,U),NNIL*LIsT(X)))∧
    (∀X U.(∀U3 X.sL(U3,U)⊃sL(CONs(X,U3),U*LIsT(X)))⊃
           (∀U2 X1.sL(U2,CONs(X,U))⊃sL(CONs(X1,U2),CONs(X,U)*LIsT(X1))))⊃
     (∀U U1 X.sL(U1,U)⊃sL(CONs(X,U1),U*LIsT(X)))
    ctxt: (1 10 LIsPAX#1 LIsPAX#2 LIsPAX#5 LIsPAX#6 LIsPAX#18 LIsPAX#22)
    deps: NIL

(DECs |∀X U.sL(U,NNIL)⊃CONs(X,U)=NNIL*LIsT(X)| |NIL| (7 6 LIsPAX#20 LIsPAX#24)
 NIL LIsPAX#12 LIsPAX#23 LIsPAX#19)
11. ∀X U.sL(U,NNIL)⊃CONs(X,U)=NNIL*LIsT(X)
    ctxt: (1 LIsPAX#1 LIsPAX#2 LIsPAX#5 LIsPAX#6 LIsPAX#18 LIsPAX#22)
    deps: NIL

(decsimp samelength#10#1#1 nil (11 8) nil (lispax#12 lispax#23 lispax#19))
(assume |u=v|)
(decsimp |sl(u,v)| nil (* 8) nil nil 12)
n
12. U=V
    ctxt: (LIsPAX#1)   deps: (12)

* decide: cannot prove the following :
U=V∧(∀U.sL(U,U))⊃sL(U,V)
want to assume these?(y or n): eh? try again
decide: cannot prove the following :
U=V⊃sL(U,V)
want to assume these?(y or n): o.k.
* decide: cannot prove the following :
(∀U4.sL(U4,U4))⊃sL(V,V)
want to assume these?(y or n): 

(decide |(∀u.sl(u,u)) ⊃ (∀u v.u=v ⊃ sl(u,v))|)
* 13. (∀U.sL(U,U))⊃(∀U V.U=V⊃sL(U,V))
    ctxt: (1 LIsPAX#1)   deps: NIL

* decide: cannot prove the following :
(∀U5 V1.U5=V1⊃sL(U5,V1))∧(∀U6.sL(U6,U6))⊃sL(V,V)
want to assume these?(y or n): 
n
o.k.
(save-proofs sl1)
.....done.
* 
proof? 
* 
(show)
.....done.sAMELENGTH read in 
LIsPAX read in 
sAMELE read in 
proof? 
* switched to sAMELENGTH
* (DECL (sL) |GROUND⊗GROUND→TRUTHVAL| CONsTANT)

(AXIOM |∀U V.sL(U,V)≡NULL(U)∧NULL(V)∨(¬NULL(U)∧¬NULL(V))∧sL(CDR(U),CDR(V))|)
2. ∀U V.sL(U,V)≡NULL(U)∧NULL(V)∨¬NULL(U)∧¬NULL(V)∧sL(CDR(U),CDR(V))
   ctxt: (1 LIsPAX#1 LIsPAX#7 LIsPAX#8)   deps: NIL

(∀E U |U| 2 |NIL|)
3. ∀V.sL(U,V)≡NULL(U)∧NULL(V)∨¬NULL(U)∧¬NULL(V)∧sL(CDR(U),CDR(V))
   ctxt: (1 LIsPAX#1 LIsPAX#7 LIsPAX#8)   deps: NIL

(∀E V |NNIL| 3 |NIL|)
4. sL(U,NNIL)≡NULL(U)∧NULL(NNIL)∨¬NULL(U)∧¬NULL(NNIL)∧sL(CDR(U),CDR(NNIL))
   ctxt: (1 LIsPAX#1 LIsPAX#5 LIsPAX#7 LIsPAX#8)   deps: NIL

(DECs |NULL(NNIL)| |$NIL#13*NIL|)
5. NULL(NNIL)
   ctxt: (LIsPAX#5 LIsPAX#8)   deps: NIL

(DECs |sL(U,NNIL)≡U=NNIL| |$NIL#13*NIL| 4 5)
6. sL(U,NNIL)≡U=NNIL
   ctxt: (1 LIsPAX#1 LIsPAX#5)   deps: NIL

(∀E PHI |λU.sL(U,U)| LIsPAX#17 |NIL| LIsPAX#12)
7. sL(NNIL,NNIL)∧(∀X U.sL(U,U)⊃sL(CONs(X,U),CONs(X,U)))⊃(∀U.sL(U,U))
   ctxt: (1 LIsPAX#1 LIsPAX#2 LIsPAX#5 LIsPAX#6)   deps: NIL

(DECs |∀U.sL(U,U)| |NIL| (7 2 6 5) NIL LIsPAX#12)
8. ∀U.sL(U,U)
   ctxt: (1 LIsPAX#1)   deps: NIL

(∀I (U) 6)
9. ∀U.sL(U,NNIL)≡U=NNIL
   ctxt: (1 LIsPAX#1 LIsPAX#5)   deps: NIL

(∀E PHI |λV.∀U X Y.sL(U,V)⊃sL(CONs(X,U),V*LIsT(X))| LIsPAX#17 |NIL| LIsPAX#12)
10. (∀U X.sL(U,NNIL)⊃sL(CONs(X,U),NNIL*LIsT(X)))∧
    (∀X U.(∀U3 X.sL(U3,U)⊃sL(CONs(X,U3),U*LIsT(X)))⊃
           (∀U2 X1.sL(U2,CONs(X,U))⊃sL(CONs(X1,U2),CONs(X,U)*LIsT(X1))))⊃
     (∀U U1 X.sL(U1,U)⊃sL(CONs(X,U1),U*LIsT(X)))
    ctxt: (1 10 LIsPAX#1 LIsPAX#2 LIsPAX#5 LIsPAX#6 LIsPAX#18 LIsPAX#22)
    deps: NIL

(DECL (U U0 U1 U2 U3 V V0 V1 V2 V3 W W0 W1 W2 W3) |GROUND| VARIABLE LIsTP)

(DECL (X Y Z) |GROUND| VARIABLE sEXP)

(DECL (A B C) |GROUND| VARIABLE)

(DECL (PHI) |GROUND→TRUTHVAL| VARIABLE)

(DECL (NNIL) |GROUND| CONsTANT LIsTP)

(DECL (CONs) |GROUND⊗GROUND→GROUND| CONsTANT)

(DECL (CAR CDR) |GROUND→GROUND| CONsTANT)

(DECL (NULL) |GROUND→TRUTHVAL| CONsTANT)

(DECL (LIsTP) |GROUND→TRUTHVAL| CONsTANT)

(DECL (sEXP) |GROUND→TRUTHVAL| CONsTANT)

11. ∀U.sEXP(U)

12. ∀X U.LIsTP(CONs(X,U))

13. ∀U.NULL(U)≡U=NNIL

14. ∀X U.¬NULL(CONs(X,U))

15. ∀X U.CAR(CONs(X,U))=X

16. ∀X U.CDR(CONs(X,U))=U

17. ∀PHI.PHI(NNIL)∧(∀X U.PHI(U)⊃PHI(CONs(X,U)))⊃(∀U.PHI(U))

(DECL (*) |GROUND⊗GROUND→GROUND| CONsTANT NIL INFIX 840)

19. ∀U V.LIsTP(U*V)

20. ∀U V.U*V=IF NULL(U) THEN V ELsE CONs(CAR(U),CDR(U)*V)

(DECL (REVERsE LIsT1) |GROUND→GROUND| CONsTANT)

(DECL (LIsT) |(GROUND*→GROUND)| FUNCTIONAL)

23. ∀X.LIsTP(LIsT(X))

24. ∀X.LIsT(X)=CONs(X,NNIL)

25. ∀X Y.LIsTP(LIsT(X,Y))

26. ∀X Y.LIsT(X,Y)=CONs(X,LIsT(Y))

27. ∀X Y Z.LIsTP(LIsT(X,Y,Z))

28. ∀X Y Z.LIsT(X,Y,Z)=CONs(X,LIsT(Y,Z))

29. ∀U.LIsTP(REVERsE(U))

30. ∀U.REVERsE(U)=IF NULL(U) THEN NNIL ELsE REVERsE(CDR(U))*LIsT(CAR(U))

31. ∀U V W.(U*V)*W=U*(V*W)

32. ∀X U V.CONs(X,U*V)=CONs(X,U)*V

33. ∀U V.REVERsE(U*V)=REVERsE(V)*REVERsE(U)